Theorem Proving in Lean 4
良いらしい
1. イントロダクション
コンピューターが主張の立証に役立つ方法は2つある:
1つは、そもそも証明を「発見」する手助けをすること、
もう1つは証明とされるものが正しいかどうかを「検証」する手助けをすることである。
Automated theorem proving(自動定理証明)は、この「発見」の側面に焦点を当てている。 対照的に、interactive theorem proving(対話型定理証明)は、定理証明の「検証」の側面に焦点を当て、全ての主張が適切な公理的基礎づけにおける証明によって保証されることを要求する。 2. 依存型理論
a countable hierarchy of non-cumulative universes and inductive typesってなに
\toなどで$ \toが補完されるの良いねmrsekut.icon
pursやjuliaでも採用するとええね
常にtexというわけでもないんだ
\aでαが出せる
$ \timesは\timesでも\xでも良い
\<1文字アルファベット>を見てみた
code:_
α -- a
β -- b
χ -- c
↓ -- d
ε -- e
‹ -- f
γ -- g
⟶ -- h
∩ -- i
⊔ -- j
κ -- k
← -- l
μ -- m
¬ -- n
∘ -- o
Π -- p
∎ -- q
→ -- r
σ -- s
▸ -- t
↑ -- u
∨ -- v
℘ -- w
× -- x
¥ -- y
ζ -- z
code:_
𝔸 -- A
□ -- B
ℂ -- C
Δ -- D
Η -- E
𝔽 -- F
Γ -- G
ℍ -- H
⋂ -- I
⨆ -- J
𝕂 -- K
Λ -- L
𝐴 -- M
ℕ -- N
Ø -- O
Π -- P
ℚ -- Q
ℝ -- R
Σ -- S
◀ -- T
⋃ -- U
‖ -- V
\W -- W なぜか割り当てがない
⨯ -- X
Ϳ -- Y
ℤ -- Z
割とバラバラ
よく使うものを良い感じに割り当ててるのだね
local definitions
code:lean
#check let y := 2 + 2; y * y -- Nat #eval let y := 2 + 2; y * y -- 16 code:lean
def double_square (x : Nat) : Nat :=
let y := x + x; y * y
改行すれば;を省略できる
code:lean
def fouble_square (x : Nat) : Nat :=
let y := x + x
y * y
hsのlet..inと同じ
example コマンドは、定理に名前を付けたり、永続する文脈に定理を保存することなく、定理を記述するのに使う。基本的には、example コマンドは与えられた項が与えられた型を持っているかどうかをチェックするだけである。実例を示すのに便利で、よく使うコマンドである。
項の型チェック
項の評価
code:lean
#check Nat.add -- Nat → Nat → Nat #check Nat.add 3 -- Nat → Nat 部分適用できるのね #check (5, 9).2 -- Nat fst/sndを.1/.2で書けるのね 型の型
code:lean
-- ..
#check Type 33 -- maximum universe level offset threshold (32) has been reached, you can increase the limit using option set_option maxUniverseOffset <limit>, but you are probably misusing universe levels since offsets are usually small natural numbers これが、非累積的宇宙の可算無限階層ってこと？
table:_
sort Prop (Sort 0) Type (Sort 1) Type 1 (Sort 2) Type 2 (Sort 3) ...
type(型) True Bool Nat -> Type Type -> Type 1 ...
term(項) trivial true fun n => Fin n fun (_ : Type) => Type ...
Type 0
Natなどの普通の型たちからなる宇宙
TypeはType 0の略称
Type 1
Type 0を項に持つより大きい宇宙
..
trueとは別にTrueがあるのか
依存型だから？
true : Bool
True : Prop
universeを使って定義する
code:lean
universe u
def F (α : Type u) : Type u := Prod α α -- Type u に属する型 α を受け取ると、α と α の直積型を返す関数
多層な項を定義する際に使える
universeを使わずに各方法もある
code:lean
def F.{u} (α : Type u) : Type u := Prod α α
名前空間
いったんするー
What makes dependent type theory dependent? (何が依存型理論を依存たらしめているのか？)
consという関数の型を考える
cons α :: α -> List α -> αとなるのはわかる
第1引数はgenerics的なものだと捉えれば良い
では、cons自体の型は？
(α : Type) → α → List α → List α
型(α)自体に型(Type)がついている
型を引数に取ることと、genericsとして定義することの違いは #?? 何なら型を入力引数として与えることもできる:
code:lean
#check fun (α β γ : Type) (g : β → γ) (f : α → β) (x : α) => g (f x) Implicit Arguments (暗黙の引数)
3. 命題と証明
型としての命題
code:lean
def Implies (p q : Prop) : Prop := p → q
#check And -- Prop → Prop → Prop #check Or -- Prop → Prop → Prop #check Implies -- Prop → Prop → Prop variable (p q r : Prop)
#check Implies (And p q) (And q p) -- Prop Propが命題を表す型
Type 0に属する
And, Ordなどはコンストラクタ
命題から命題を構築する
しれっと出てきたProofが何なのかわからん #?? code:lean
structure Proof (p : Prop) : Type where
proof : p
show
項の型を明示できる？
項に型注釈する際に使う？
以下は同じ
code:lean
theorem t1 : p → q → p := fun hp : p => fun hq : q => hp
code:lean
theorem t1 : p → q → p :=
fun hp : p =>
fun hq : q =>
show p from hp -- show <型> from <項>
True, False, Not
/\
\/
->
<->
命題論理のやつ
Prop型を引数に取り、Props型を返す
/\型のconstructorみたいなイメージかな
code:lean
variable (p q : Prop)
example (hp:p) (hq:q) : p /\ q := And.intro hp hq
code:lean
variable (p q : Prop)
example (h : p ∧ q) : p := And.left h
example (h : p ∧ q) : q := And.right h
code:lean
variable (p q : Prop)
example (h : p ∧ q) : p := And.left h
example (h : p ∧ q) : q := And.right h
前節ではラムダ抽象を → の「導入則」とみなすことができることを説明した。ラムダ抽象が含意命題を「導入」あるいは構築する方法だとすると、関数適用は「含意の除去則」だとみなせる。つまり、関数適用は証明の中で含意を「除去する」あるいは使う方法である。ref 例題
p ∧ q → q ∧ pを証明してみよう
手順
軽く証明するならexampleを使えば良い
型としては、example (h : p /\ q): q /\ p :=
連言導入、左/右連言除去則を使う
And.intro (And.right h) (And.left h)が答え
匿名コンストラクタ
/\に特有なもの？よくわからん
違いそう
割と可読性が落ちると思う
code:lean
methodを生やす感じで関数を呼べる
code:lena
variable (xs : List Nat)
Or.intro_left q hp
code:lean
variable (p q : Prop)
example (hp : p) : p ∨ q := Or.intro_left q hp
Or.intro_right p hq
code:lean
variable (p q : Prop)
example (hq : q) : p ∨ q := Or.intro_right p hq
⊢ ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c
if文ぽいものを書く必要がある
使用例: p ∨ q → q ∨ pの証明
code:lean
example (h : p ∨ q) : q ∨ p :=
Or.elim h -- r
(fun hp : p => -- pからrを導ける
show q ∨ p from Or.intro_right q hp)
(fun hq : q => -- qからrを導ける
show q ∨ p from Or.intro_left p hq)
矛盾から任意の命題が導かれる
code:lean
variable (p q : Prop)
example (hp : p) (hnp : ¬p) : q := False.elim (hnp hp)
absurd
恒偽から導かれる任意の命題 q は暗黙の引数であり、自動的に型推論される。矛盾する前提から任意の命題を導くパターンは非常によく見られ、absurd で表現される。
h1 : p → q と h2 : q → p から p ↔ q の証明を作る
h : p ↔ q から p → q の証明を作る
h : p ↔ q から q → p の証明を作る
このへんから
4. 量化子と等号
5. タクティク
6. Leanとの対話
7. 帰納型
逆に、宇宙と依存関数型はfoundational types(基礎型)として知られる)
8. 帰納と再帰
9. 構造体とレコード
10. 型クラス
11. 変換タクティクモード
12. 公理と計算